<html>
<head><meta charset="utf-8"><title>Generativity / Invariant Lifetimes / Branded Types · general · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/index.html">general</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Generativity.20.2F.20Invariant.20Lifetimes.20.2F.20Branded.20Types.html">Generativity / Invariant Lifetimes / Branded Types</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="248691141"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Generativity%20/%20Invariant%20Lifetimes%20/%20Branded%20Types/near/248691141" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Zoey <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Generativity.20.2F.20Invariant.20Lifetimes.20.2F.20Branded.20Types.html#248691141">(Aug 07 2021 at 02:46)</a>:</h4>
<p>Hello - I'm trying to understand "Branded Types" more thoroughly, and- while lifetimes can be used to perform this trick (a la <a href="https://crates.io/crates/generativity">generativity</a> or <a href="http://plv.mpi-sws.org/rustbelt/ghostcell/">Ghost Cell</a>)- I'm at a bit of a loss for understanding how to translate this concept into other type systems.</p>
<p>I'm attempting to create a function which produces a result of some type T with genericity such that two outputs from the function are _incompatible_ with eachother for some binary associative functions until they are proven to share the same "brand" value via a runtime check.</p>
<p>My assumption is that I can return <code>T&lt;'brand&gt;</code> where 'brand is guaranteed unique per invocation, provide an impl:</p>
<div class="codehilite" data-code-language="Rust"><pre><span></span><code><span class="k">impl</span><span class="o">&lt;'</span><span class="na">brand</span><span class="o">&gt;</span><span class="w"> </span><span class="n">MyBrandedType</span><span class="o">&lt;'</span><span class="na">brand</span><span class="o">&gt;</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">  </span><span class="k">pub</span><span class="w"> </span><span class="k">fn</span> <span class="nf">into_compatible</span><span class="o">&lt;</span><span class="n">Other</span>: <span class="nc">MyBrandedType</span><span class="o">&lt;'</span><span class="na">other</span><span class="o">&gt;&gt;</span><span class="p">(</span><span class="w"></span>
<span class="w">    </span><span class="bp">self</span><span class="p">,</span><span class="w"></span>
<span class="w">    </span><span class="n">other</span>: <span class="kp">&amp;</span><span class="nc">Other</span><span class="w"></span>
<span class="w">  </span><span class="p">)</span><span class="w"> </span>-&gt; <span class="nb">Result</span><span class="o">&lt;</span><span class="n">MyBrandedType</span><span class="o">&lt;'</span><span class="na">other</span><span class="o">&gt;</span><span class="p">,</span><span class="w"> </span><span class="bp">Self</span><span class="o">&gt;</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">    </span><span class="k">if</span><span class="w"> </span><span class="n">do_my_runtime_compatible_check</span><span class="o">!</span><span class="p">(</span><span class="o">&amp;</span><span class="bp">self</span><span class="p">,</span><span class="w"> </span><span class="n">other</span><span class="p">)</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">      </span><span class="c1">// use phantomdata::default to instantiate a new instance with the 'other lifetime</span>
<span class="w">      </span><span class="nb">Ok</span><span class="p">(</span><span class="fm">todo!</span><span class="p">())</span><span class="w"></span>
<span class="w">    </span><span class="p">}</span><span class="w"> </span><span class="k">else</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">      </span><span class="nb">Err</span><span class="p">(</span><span class="bp">self</span><span class="p">)</span><span class="w"></span>
<span class="w">    </span><span class="p">}</span><span class="w"></span>
<span class="w">  </span><span class="p">}</span><span class="w"></span>
<span class="p">}</span><span class="w"></span>
</code></pre></div>
<p>But ... What does this map to in something like Haskell's type system, where lifetimes are not present? Am I overlooking something with regards to the compatibility of invariant lifetimes?</p>
<p>I suspect the core aspect of the idea is that of proving that two items with runtime data are or are not compatible at compile time, despite the actual <code>subtypes</code> of that data being statically unknowable. Is there some other way to represent such a scenario with compile-time enforcement?</p>



<a name="248692362"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Generativity%20/%20Invariant%20Lifetimes%20/%20Branded%20Types/near/248692362" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Generativity.20.2F.20Invariant.20Lifetimes.20.2F.20Branded.20Types.html#248692362">(Aug 07 2021 at 03:16)</a>:</h4>
<p>The technique of branded types looks very similar to the existential type trick used to make <a href="https://hackage.haskell.org/package/base-4.15.0.0/docs/Control-Monad-ST.html#v:runST"><code>runST</code></a> and <code>ST</code>-refs work. In particular, multiple calls to <code>runST</code> get distinct, quantified type variables, much like the lifetime variable <code>'brand</code> in this example.</p>



<a name="248692440"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Generativity%20/%20Invariant%20Lifetimes%20/%20Branded%20Types/near/248692440" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Generativity.20.2F.20Invariant.20Lifetimes.20.2F.20Branded.20Types.html#248692440">(Aug 07 2021 at 03:17)</a>:</h4>
<p>Rust can't express <code>runST</code> because it doesn't have functions with type quantifiers - you can have <code>for&lt;'a&gt; fn(T&lt;'a&gt;)</code> but not <code>for&lt;X&gt; fn(T&lt;X&gt;)</code></p>



<a name="248693468"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Generativity%20/%20Invariant%20Lifetimes%20/%20Branded%20Types/near/248693468" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Zoey <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Generativity.20.2F.20Invariant.20Lifetimes.20.2F.20Branded.20Types.html#248693468">(Aug 07 2021 at 03:40)</a>:</h4>
<p>How does X differ from a generic <code>X</code> on an <code>impl&lt;X&gt;</code>; do type quantifiers not need constrained? It looks like type quantifiers would arrive as a part of HKT, if Rust were to add it, if I am understanding correctly where the representation hole exists?</p>



<a name="248693755"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Generativity%20/%20Invariant%20Lifetimes%20/%20Branded%20Types/near/248693755" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Generativity.20.2F.20Invariant.20Lifetimes.20.2F.20Branded.20Types.html#248693755">(Aug 07 2021 at 03:46)</a>:</h4>
<p>No, here we're talking about a single function pointer that can accept multiple types. It might be possible to do this with some kind of <code>dyn</code>, but for the most part the rust type system is not set up to do this in the same way as haskell</p>



<a name="248693871"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Generativity%20/%20Invariant%20Lifetimes%20/%20Branded%20Types/near/248693871" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Mario Carneiro <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Generativity.20.2F.20Invariant.20Lifetimes.20.2F.20Branded.20Types.html#248693871">(Aug 07 2021 at 03:49)</a>:</h4>
<p>I'm not sure what HKT proposals look like these days, but I imagine that they would be handled using static dispatch (<code>impl</code> not <code>dyn</code>), and it would almost certainly not be object safe because of the generics</p>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>